(set-logic QF_LIA)
(set-info :source |
    Sequential equivalence checking.
    Calypto Design Systems, Inc. <www.calypto.com>
  |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun P_2 () Int)
(declare-fun P_3 () Bool)
(declare-fun P_4 () Bool)
(declare-fun P_5 () Bool)
(declare-fun P_6 () Bool)
(declare-fun P_7 () Bool)
(declare-fun P_8 () Bool)
(declare-fun P_9 () Int)
(declare-fun P_10 () Int)
(declare-fun P_11 () Int)
(declare-fun P_12 () Int)
(declare-fun P_13 () Bool)
(declare-fun P_14 () Bool)
(declare-fun P_15 () Bool)
(declare-fun P_16 () Bool)
(declare-fun P_17 () Bool)
(declare-fun P_18 () Bool)
(declare-fun P_19 () Bool)
(declare-fun P_20 () Bool)
(declare-fun P_21 () Bool)
(declare-fun P_22 () Bool)
(declare-fun P_23 () Bool)
(declare-fun P_24 () Bool)
(declare-fun P_25 () Bool)
(declare-fun P_26 () Bool)
(declare-fun P_27 () Bool)
(declare-fun P_28 () Bool)
(declare-fun P_29 () Bool)
(declare-fun P_30 () Bool)
(declare-fun P_31 () Bool)
(declare-fun P_32 () Int)
(declare-fun P_33 () Int)
(declare-fun P_34 () Bool)
(declare-fun P_35 () Bool)
(declare-fun P_36 () Bool)
(declare-fun P_37 () Bool)
(declare-fun P_42 () Bool)
(declare-fun P_43 () Bool)
(declare-fun P_44 () Bool)
(declare-fun P_45 () Bool)
(declare-fun P_46 () Bool)
(declare-fun P_47 () Bool)
(declare-fun P_48 () Bool)
(declare-fun P_49 () Bool)
(assert (<= (- 512) P_2))
(assert (<= P_2 511))
(assert (<= 0 P_9))
(assert (<= P_9 3))
(assert (<= 0 P_10))
(assert (<= P_10 255))
(assert (<= (- 512) P_11))
(assert (<= P_11 511))
(assert (<= (- 128) P_12))
(assert (<= P_12 127))
(assert (<= 0 P_32))
(assert (<= P_32 3))
(assert (<= 0 P_33))
(assert (<= P_33 3))
(declare-fun dz () Int)
(declare-fun rz () Int)
(assert (let ((?v_2 (< P_2 0)) (?v_4 (+ 512 (+ (ite P_3 256 0) (+ (ite P_4 128 0) (+ (ite P_5 64 0) (+ (ite P_6 32 0) (+ (ite P_7 16 0) (+ (ite P_8 8 0) (+ (* P_9 2) 1))))))))) (?v_0 (+ (- (- (- 2) (* 2 P_10)) (- 512)) 1))) (let ((?v_1 (< (- (+ ?v_4 (ite (>= ?v_0 0) ?v_0 (+ ?v_0 512))) 1024) 0))) (let ((?v_3 (and ?v_2 (not ?v_1))) (?v_6 (and ?v_1 (not ?v_2))) (?v_5 (+ (- (* 2 P_12) (- 512)) 1))) (let ((?v_7 (- (+ (ite (or (and (not (< P_11 0)) ?v_3) (and (not (< (- (+ ?v_4 (ite (>= ?v_5 0) ?v_5 (+ ?v_5 512))) 1024) 0)) ?v_6)) 1 0) 1) 2))) (let ((?v_8 (+ (ite (or ?v_3 ?v_6) 2 0) (ite (>= ?v_7 0) ?v_7 (+ ?v_7 2))))) (let ((?v_9 (= ?v_8 0)) (?v_10 (= ?v_8 1)) (?v_11 (= ?v_8 2))) (let ((?v_12 (ite ?v_10 P_14 (ite ?v_11 P_3 P_15))) (?v_13 (ite ?v_10 P_17 (ite ?v_11 P_4 P_18))) (?v_14 (ite ?v_10 P_20 (ite ?v_11 P_5 P_21))) (?v_15 (ite ?v_10 P_23 (ite ?v_11 P_6 P_24))) (?v_16 (ite ?v_10 P_26 (ite ?v_11 P_7 P_27))) (?v_17 (ite ?v_10 P_29 (ite ?v_11 P_8 P_30))) (?v_18 (ite ?v_10 (< (ite (< P_32 2) P_32 (- P_32 4)) 0) (ite ?v_11 (< (ite (< P_9 2) P_9 (- P_9 4)) 0) (< (ite (< P_33 2) P_33 (- P_33 4)) 0)))) (?v_19 (ite ?v_10 P_35 (ite ?v_11 P_36 P_37)))) (= (+ (* 256 dz) rz) (- (+ (ite (ite ?v_9 P_42 ?v_12) 128 0) (+ (ite (ite ?v_9 P_43 ?v_13) 64 0) (+ (ite (ite ?v_9 P_44 ?v_14) 32 0) (+ (ite (ite ?v_9 P_45 ?v_15) 16 0) (+ (ite (ite ?v_9 P_46 ?v_16) 8 0) (+ (ite (ite ?v_9 P_47 ?v_17) 4 0) (+ (ite (ite ?v_9 P_48 ?v_18) 2 0) (ite (ite ?v_9 P_49 ?v_19) 1 0)))))))) (+ (ite (ite ?v_9 P_13 ?v_12) 128 0) (+ (ite (ite ?v_9 P_16 ?v_13) 64 0) (+ (ite (ite ?v_9 P_19 ?v_14) 32 0) (+ (ite (ite ?v_9 P_22 ?v_15) 16 0) (+ (ite (ite ?v_9 P_25 ?v_16) 8 0) (+ (ite (ite ?v_9 P_28 ?v_17) 4 0) (+ (ite (ite ?v_9 P_31 ?v_18) 2 0) (ite (ite ?v_9 P_34 ?v_19) 1 0))))))))))))))))))
(assert (> rz 0))
(assert (< rz 256))
(check-sat)
(exit)
